
(set-info :smt-lib-version 2.6)
(set-logic QF_FFA)
(define-sort FF0 () (_ FiniteField 3))
(declare-fun x0 () FF0)
(declare-fun x1 () FF0)
(declare-fun x2 () FF0)
(declare-fun x3 () FF0)
(declare-fun x4 () FF0)
(declare-fun x5 () FF0)
(declare-fun x6 () FF0)
(declare-fun x7 () FF0)
(assert
  (let ((let0 (ff.mul x2 x2 x2)))
  (let ((let1 (ff.mul x0 x2 x3)))
  (let ((let2 (ff.mul x1 x4 x5)))
  (let ((let3 (ff.mul (as ff2 FF0) x0 x2 x6)))
  (let ((let4 (ff.mul (as ff2 FF0) x0 x5)))
  (let ((let5 (as ff1 FF0)))
  (let ((let6 (ff.add let0 let1 let2 let3 let4 let5)))
  (let ((let7 (= let6 (as ff0 FF0))))
  (let ((let8 (ff.mul (as ff2 FF0) x2 x4 x5)))
  (let ((let9 (ff.mul x2 x2 x6)))
  (let ((let10 (ff.mul (as ff2 FF0) x0 x1 x7)))
  (let ((let11 (ff.mul (as ff2 FF0) x2 x5 x7)))
  (let ((let12 (ff.mul x2 x7)))
  (let ((let13 (ff.add let8 let9 let10 let11 let12)))
  (let ((let14 (= let13 (as ff0 FF0))))
  (let ((let15 (ff.mul (as ff2 FF0) x6 x6 x6)))
  (let ((let16 (ff.mul (as ff2 FF0) x3 x7 x7)))
  (let ((let17 (ff.mul (as ff2 FF0) x1 x5)))
  (let ((let18 (ff.mul (as ff2 FF0) x1 x6)))
  (let ((let19 (ff.add let15 let16 let17 let18)))
  (let ((let20 (= let19 (as ff0 FF0))))
  (let ((let21 (ff.mul x2 x2 x5)))
  (let ((let22 (ff.mul x4 x7)))
  (let ((let23 (ff.add let21 let22)))
  (let ((let24 (= let23 (as ff0 FF0))))
  (let ((let25 (ff.mul x0 x0 x2)))
  (let ((let26 (= let25 (as ff0 FF0))))
  (let ((let27 (ff.mul (as ff2 FF0) x0 x3 x7)))
  (let ((let28 (ff.mul (as ff2 FF0) x2 x4 x7)))
  (let ((let29 (as ff2 FF0)))
  (let ((let30 (ff.add let27 let28 let29)))
  (let ((let31 (= let30 (as ff0 FF0))))
  (let ((let32 (ff.mul (as ff2 FF0) x1 x3 x4)))
  (let ((let33 (ff.mul (as ff2 FF0) x6 x6 x6)))
  (let ((let34 (ff.mul x2 x2)))
  (let ((let35 (ff.mul (as ff2 FF0) x4 x4)))
  (let ((let36 (ff.mul (as ff2 FF0) x4 x6)))
  (let ((let37 (ff.add let32 let33 let34 let35 let36)))
  (let ((let38 (= let37 (as ff0 FF0))))
  (let ((let39 (ff.mul (as ff2 FF0) x4 x5 x5)))
  (let ((let40 (ff.mul (as ff2 FF0) x1 x2 x6)))
  (let ((let41 (ff.mul x5 x6 x6)))
  (let ((let42 (ff.mul x0 x4)))
  (let ((let43 (ff.add let39 let40 let41 let42)))
  (let ((let44 (= let43 (as ff0 FF0))))
  (let ((let45 (and let7 let14 let20 let24 let26 let31 let38 let44)))
  let45
))))))))))))))))))))))))))))))))))))))))))))))
)
(check-sat)
